Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern void abort(void); |
2 | extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
3 | void reach_error() { __assert_fail("0", "loop4.c", 10, "reach_error"); } |
4 | void assume_abort_if_not(int cond) { |
5 | if(!cond) {abort();} |
6 | } |
7 | void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } } |
8 | extern int __VERIFIER_nondet_int(void); |
9 | extern void __VERIFIER_assume(int); |
10 | |
11 | int main() { |
12 | int x,y; |
13 | x = 0; |
14 | y = 0; |
15 | while (1) { |
16 | if (x < 50) { |
17 | y++; |
18 | } else { |
19 | y--; |
20 | } |
21 | if (y < 0) break; |
22 | x++; |
23 | } |
24 | __VERIFIER_assert(x == 100); |
25 | return 0; |
26 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2023-07-13 | 03:07:16:037 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2023-07-13 | 03:07:16:054 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-07-13 | 03:07:16:103 | INFO | CPAchecker.run | CPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started |
| 2023-07-13 | 03:07:16:119 | INFO | CPAchecker.parse | Parsing CFA from file(s) "no_context/loop4.c" |
| 2023-07-13 | 03:07:16:922 | INFO | CoreComponentsFactory.createAlgorithm | Using heuristics to select analysis |
| 2023-07-13 | 03:07:16:932 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions termination.violation.witness cpa.predicate.memoryAllocationsAlwaysSucceed cpa.arg.compressWitness cpa.callstack.skipFunctionPointerRecursion cpa.composite.aggregateBasicBlocks counterexample.export.graphml counterexample.export.compressWitness cpa.arg.proofWitness |
| 2023-07-13 | 03:07:16:932 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2023-07-13 | 03:07:16:936 | INFO | SelectionAlgorithm.chooseConfig | Performing heuristic ... |
| 2023-07-13 | 03:07:16:954 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-07-13 | 03:07:16:957 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2023-07-13 | 03:07:16:963 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties RestartAlgorithm.run | Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties ... |
| 2023-07-13 | 03:07:16:967 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'. |
| 2023-07-13 | 03:07:16:968 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'. |
| 2023-07-13 | 03:07:16:970 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'. |
| 2023-07-13 | 03:07:16:972 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 140s |
| 2023-07-13 | 03:07:17:232 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties RestartAlgorithm.run | Starting analysis 1 ... |
| 2023-07-13 | 03:07:17:642 | INFO | CPAchecker.runAlgorithm | Stopping analysis ... |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Selection Algorithm statistics | ||
| Size of preliminary analysis reached set | 0 | |
| Used algorithm property | /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties | |
| Program containing only relevant bools | 0 | |
| Relevant boolean vars / relevant vars ratio | 0.1667 | |
| Requires alias handling | 0 | |
| Requires loop handling | 1 | |
| Has a single loop | 1 | |
| Requires composite-type handling | 0 | |
| Requires array handling | 0 | |
| Requires float handling | 0 | |
| Requires recursion handling | 0 | |
| Relevant addressed vars / relevant vars ratio | 0.0000 | |
| Program containing external functions | true | |
| Number of all righthand side functions | 4 | |
| Restart Algorithm statistics | ||
| Number of algorithms provided | 7 | |
| Number of algorithms used | 1 | |
| Total time for algorithm 1 | 0.679s | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 4.47 | sum: 3204, count: 716, min: 0, max: 6 |
| Number of global variables per state | 0.00 | sum: 0, count: 716, min: 0, max: 0 |
| Number of assumptions | 812 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 715 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.014s | |
| Total time for path thresholds | 0.000s | |
| SymbolicValueAnalysisPrecisionAdjustment statistics | ||
| Symbolic values before refinement | 0 | count: 715, min: 0, max: 0, avg: 0.00 |
| Symbolic values after refinement | 0 | count: 715, min: 0, max: 0, avg: 0.00 |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.003s | |
| Replaced symbolic expressions | 0 | |
| ConstraintsCPA statistics | ||
| Time for solving constraints | 0.079s | |
| Time for SMT check | 0.000s | |
| Time for resolving definites | 0.000s | |
| Cache lookups | 203 | |
| Direct cache hits | 202 | |
| Direct cache lookup time | 0.000s | |
| Subset cache hits | 0 | |
| Subset cache lookup time | 0.000s | |
| Superset cache hits | 0 | |
| Superset cache lookup time | 0.000s | |
| Number of removed outdated constraints | 0 | count: 203, min: 0, max: 0, avg: 0.00 |
| Time for outdated constraint removal | 0.009s | |
| Constraints after refinement in state | 0 | count: 715, min: 0, max: 0, avg: 0.00 |
| Constraints before refinement in state | 0 | count: 715, min: 0, max: 0, avg: 0.00 |
| Time for constraints adjustment | 0.005s | |
| AutomatonAnalysis (SVCOMP) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.023s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 1129, count: 1129, min: 1, max: 1 [1 x 1129] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 716 | |
| Max size of waitlist | 1 | |
| Average size of waitlist | 1 | |
| Number of computed successors | 715 | |
| Max successors for one state | 1 | |
| Number of times merged | 0 | |
| Number of times stopped | 0 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.399s | Max: 0.399s |
| Time for choose from waitlist | 0.000s | |
| Time for precision adjustment | 0.059s | |
| Time for transfer relation | 0.266s | |
| Time for stop operator | 0.054s | |
| Time for adding to reached set | 0.002s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 716 | |
| Max size of waitlist | 1 | |
| Average size of waitlist | 1 | |
| Number of computed successors | 715 | |
| Max successors for one state | 1 | |
| Number of times merged | 0 | |
| Number of times stopped | 0 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.399s | Max: 0.399s |
| Time for choose from waitlist | 0.000s | |
| Time for precision adjustment | 0.059s | |
| Time for transfer relation | 0.266s | |
| Time for stop operator | 0.054s | |
| Time for adding to reached set | 0.002s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 0.500 | |
| Visited lines | 12 | |
| Total lines | 14 | |
| Line coverage | 0.857 | |
| Visited conditions | 5 | |
| Total conditions | 8 | |
| Condition coverage | 0.625 | |
| CPAchecker general statistics | ||
| Number of program locations | 55 | |
| Number of CFA edges (per node) | 52 | count: 55, min: 0, max: 2, avg: 0.95 |
| Number of relevant variables | 6 | |
| Number of functions | 4 | |
| Number of loops (and loop nodes) | 1 | sum: 15, min: 15, max: 15, avg: 15.00 |
| Size of reached set | 716 | |
| Number of reached locations | 20 | 36% |
| Avg states per location | 35 | |
| Max states per location | 101 | at node N25 |
| Number of reached functions | 2 | 50% |
| Number of target states | 0 | |
| Time for analysis setup | 0.813s | |
| Time for loading CPAs | 0.148s | |
| Time for loading parser | 0.161s | |
| Time for CFA construction | 0.475s | |
| Time for parsing file(s) | 0.228s | |
| Time for AST to CFA | 0.086s | |
| Time for CFA sanity check | 0.022s | |
| Time for post-processing | 0.072s | |
| Time for CFA export | 0.507s | |
| Time for function pointers resolving | 0.003s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.035s | |
| Time for collecting variables | 0.013s | |
| Time for solving dependencies | 0.001s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.019s | |
| Time for exporting data | 0.002s | |
| Time for Analysis | 0.709s | |
| CPU time for analysis | 2.340s | |
| Time for analyzing result | 0.001s | |
| Total time for CPAchecker | 1.524s | |
| Total CPU time for CPAchecker | 4.650s | |
| Time for statistics | 0.138s | |
| Time for Garbage Collector | 0.041s | in 4 runs |
| Garbage Collector(s) used | G1 Old Generation, G1 Young Generation | |
| Used heap memory | 76MB ( 72 MiB) max; 38MB ( 36 MiB) avg; 95MB ( 91 MiB) peak | |
| Used non-heap memory | 40MB ( 38 MiB) max; 27MB ( 26 MiB) avg; 41MB ( 39 MiB) peak | |
| Used in G1 Old Gen pool | 13MB ( 12 MiB) max; 7MB ( 7 MiB) avg; 13MB ( 12 MiB) peak | |
| Allocated heap memory | 127MB ( 122 MiB) max; 127MB ( 122 MiB) avg | |
| Allocated non-heap memory | 44MB ( 42 MiB) max; 31MB ( 30 MiB) avg | |
| Total process virtual memory | 12286MB ( 11717 MiB) max; 12042MB ( 11484 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.entryFunction | main |
| 2 | analysis.name | svcomp23 |
| 3 | analysis.programNames | no_context/loop4.c |
| 4 | analysis.selectAnalysisHeuristically | true |
| 5 | analysis.summaryEdges | true |
| 6 | cfa.simplifyCfa | false |
| 7 | cfa.useCFACloningForMultiThreadedPrograms | true |
| 8 | counterexample.export.compressWitness | false |
| 9 | counterexample.export.graphml | witness.graphml |
| 10 | cpa.arg.compressWitness | false |
| 11 | cpa.arg.proofWitness | witness.graphml |
| 12 | cpa.callstack.skipFunctionPointerRecursion | true |
| 13 | cpa.callstack.unsupportedFunctions | pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow |
| 14 | cpa.composite.aggregateBasicBlocks | false |
| 15 | cpa.predicate.memoryAllocationsAlwaysSucceed | true |
| 16 | datarace.config | svcomp23--datarace.properties |
| 17 | heuristicSelection.addressedRatio | 0.0 |
| 18 | heuristicSelection.complexLoopConfig | components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties |
| 19 | heuristicSelection.loopConfig | components/svcomp23--multipleLoopsConfig.properties |
| 20 | heuristicSelection.loopFreeConfig | components/svcomp23--configselection-restart-bmc-fallbacks.properties |
| 21 | heuristicSelection.singleLoopConfig | components/svcomp23--singleLoopConfig.properties |
| 22 | language | C |
| 23 | limits.time.cpu | 900s |
| 24 | limits.time.cpu::required | 900 |
| 25 | log.level | INFO |
| 26 | memorycleanup.config | svcomp23--memorycleanup.properties |
| 27 | memorysafety.config | svcomp23--memorysafety.properties |
| 28 | overflow.config | svcomp23--overflow.properties |
| 29 | parser.usePreprocessor | true |
| 30 | specification | /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp |
| 31 | statistics.print | true |
| 32 | termination.config | svcomp23--termination.properties |
| 33 | termination.violation.witness | witness.graphml |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}